FDL - Nuprl Definition : ecl-machine

Nuprl Definition : ecl-machine

ecl-machine{$ecl:ut2}
ecl-machine(i; ds; da; A; snd; upd)
== Rplus(ecl-machine1{$ecl:ut2}
== Rplus(ecl-machine1(i; ds; da; A);
== Rplus(spreadn(ecl-trans(A);
== Rplus(spreadn(T,ks,init,tr,h,a,es.Rplus(ecl-machine2(i; ds; da; mkid{$ecl:ut2}; T; ks; a; upd);
== Rplus(spreadn(T,ks,init,tr,h,a,es.Rplus(ecl-machine3(ds; da; mkid{$ecl:ut2}; T; ks; a; snd)))
== Rplus()

latex

Definitions mkid{$x:ut2}, ecl-machine3(ds; da; x; T; ks; a; snd), ecl-machine2(i; ds; da; x; T; ks; a; upd), Rplus(left; right), ecl-trans(x), spreadn(u; a,b,c,d,e,f,g.v(a;b;c;d;e;f;g)), ecl-machine1{$ecl:ut2}(i; ds; da; A)

FDL editor aliases esp-machine

origin

Definitions	mkid{$x:ut2}, ecl-machine3(ds; da; x; T; ks; a; snd), ecl-machine2(i; ds; da; x; T; ks; a; upd), Rplus(left; right), ecl-trans(x), spreadn(u; a,b,c,d,e,f,g.v(a;b;c;d;e;f;g)), ecl-machine1{$ecl:ut2}(i; ds; da; A)
FDL editor aliases	esp-machine